#devscripts/release.sh: Version determination for this
if [ -z "$1" ]; then echo "ERROR: specify version number like this: $0 1994.09.06"; exit 1; fi
version=`./version.sh`